|
Idris is a general-purpose purely functional programming language with dependent types. The type system is similar to the one used by Agda. The language supports interactive theorem-proving comparable to Coq, including tactics, while the focus remains on general-purpose programming even before theorem-proving. Other goals of Idris are "sufficient" performance, easy management of side-effects and support for implementing embedded domain specific languages. , Idris compiles to C and relies on a custom copying garbage collector using Cheney's algorithm. There also exist JavaScript and Java backends, and a partial LLVM backend.〔http://idris-lang.org/news〕 The name ''Idris'' goes back to the character of the singing dragon in the 70's UK kids' program Ivor the Engine.〔(【引用サイトリンク】url=http://docs.idris-lang.org/en/latest/faq/faq.html#what-does-the-name-idris-mean )〕 ==Features== Idris combines a number of features from relatively mainstream functional programming languages with features borrowed from proof assistants, in effect blurring the boundary between the two kinds of software. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Idris (programming language)」の詳細全文を読む スポンサード リンク
|